import abc
from typing import Union, Tuple, Optional, Dict, List

import model.state
from model.networktrace import NetworkTrace


class PathFormula(abc.ABC):
    def __init__(self):
        pass

    @abc.abstractmethod
    def eval(self, ns: NetworkTrace, k: int) -> bool:
        pass


class Bool(PathFormula):
    def __init__(self, value: bool):
        super().__init__()
        self.value = value

    def __eq__(self, other):
        if isinstance(other, bool):
            return self.value == other
        if isinstance(other, Bool):
            return self.value == other.value
        return False

    def __repr__(self):
        return "Bool({})".format(self.value)

    def __str__(self):
        return str(self.value)

    def eval(self, ns: NetworkTrace, k: int) -> bool:
        return self.value


class AP(PathFormula):
    def __init__(self, components: Union[str, Tuple[str, str]], key: str, comparator: str,
                 value: Union[int, float, str, Dict, List]):
        super().__init__()
        self.components = components
        self.key = key
        if comparator not in ["=", ">", ">=", "<", "<="]:
            raise ValueError("Wrong comparator")
        self.comparator = comparator
        self.value = value

    def __repr__(self):
        return "AP({}, {}, {}, {})".format(self.components, self.key, self.comparator, self.value)

    def __str__(self):
        return f"{self.components}.{self.key}{self.comparator}{self.value}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        if not self.components in nt[k].keys():
            raise ValueError("Components not in trace")
        if not self.key in nt[k][self.components].keys():
            raise ValueError("Key not in components state")

        attr_value = nt[k][self.components][self.key]
        if isinstance(attr_value, model.state.State):
            if not self.comparator == "=":
                raise ValueError("State comparator can only be =")
            return attr_value.name == self.value
        elif isinstance(attr_value, int) or isinstance(attr_value, float):
            if not self.comparator in ["=", ">", ">=", "<", "<="]:
                raise ValueError(f"{self.key} comparator can only be =, >, >=, <, <=")
            if self.comparator == ">":
                return attr_value > self.value
            if self.comparator == ">=":
                return attr_value >= self.value
            if self.comparator == "<":
                return attr_value < self.value
            if self.comparator == "<=":
                return attr_value <= self.value
            if self.comparator == "=":
                return attr_value == self.value
        else:
            if not self.comparator == "=":
                raise ValueError(f"{self.key} comparator can only be =")
            return attr_value == self.value


class Not(PathFormula):
    def __init__(self, phi):
        super().__init__()
        if not isinstance(phi, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi = phi

    def __repr__(self):
        return "Not({})".format(self.phi)

    def __str__(self):
        return f"~{self.phi}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        return not self.phi.eval(nt, k)


class And(PathFormula):
    def __init__(self, phi1, phi2):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "And({}, {})".format(self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1}&{self.phi2}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        if k > len(nt):
            return False
        return self.phi1.eval(nt, k) and self.phi2.eval(nt, k)


class Or(PathFormula):
    def __init__(self, phi1: PathFormula, phi2: PathFormula):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "Or({}, {})".format(self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1}|{self.phi2}"

    def eval(self, nt: NetworkTrace, k) -> bool:
        return self.phi1.eval(nt, k) or self.phi2.eval(nt, k)


class Imply(PathFormula):
    def __init__(self, phi1: PathFormula, phi2: PathFormula):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "Imply({}, {})".format(self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1}->{self.phi2}"

    def eval(self, nt: NetworkTrace, k) -> bool:
        return Or(Not(self.phi1), self.phi2).eval(nt, k)


class Iff(PathFormula):
    def __init__(self, phi1: PathFormula, phi2: PathFormula):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "Iff({}, {})".format(self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1}<->{self.phi2}"

    def eval(self, nt: NetworkTrace, k) -> bool:
        return And(Imply(self.phi1, self.phi2), Imply(self.phi2, self.phi1)).eval(nt, k)


class X(PathFormula):
    def __init__(self, phi: PathFormula):
        super().__init__()
        if not isinstance(phi, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi = phi

    def __repr__(self):
        return "X({})".format(self.phi)

    def __str__(self):
        return f"X({self.phi})"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        if len(nt) < k + 1:
            return False
        return self.phi.eval(nt, k + 1)

class Interval:
    def __init__(self, lo: str, lb: float, ub: float, uo: str):
        if lo not in ["[", "("]:
            raise ValueError("Wrong lower bound")
        if uo not in ["]", ")"]:
            raise ValueError("Wrong upper bound")
        if lb > ub:
            raise ValueError("Lower bound cannot be greater than upper bound")
        if lb < 0:
            raise ValueError("Lower bound cannot be negative")
        self.lo = lo
        self.lb = lb
        self.ub = ub
        self.uo = uo

    def __repr__(self):
        return f"Interval{self.lo}{self.lb}{self.uo}{self.ub}"

    def __str__(self):
        return f"{self.lo}{self.lb},{self.ub}{self.uo}"

    def include(self, t: float):
        if t < -1:
            raise ValueError("Time cannot be negative")
        if self.lo == "[":
            if self.uo == "]":
                return self.lb <= t <= self.ub
            else:
                return self.lb <= t < self.ub
        else:
            if self.uo == "]":
                return self.lb < t <= self.ub
            else:
                return self.lb < t < self.ub

class U(PathFormula):
    def __init__(self, i: Interval, phi1: PathFormula, phi2: PathFormula):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.i = i
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "U( {}, {}, {})".format(self.i, self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1} U{self.i} {self.phi2}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        time = 0
        for j in range(k, len(nt)):
            time += nt.time_trace[j]
            if not isinstance(self.phi1, Bool):
                if self.phi1.eval(nt, j):
                    continue
                else:
                    if self.phi2.eval(nt, j):
                        time -= nt.time_trace[j]
                        # if time <= self.tb:
                        if self.i.include(time):
                            return True
                        else:
                            return False
                    else:
                        return False
            else:
                if self.phi1 == Bool(True):
                    if self.phi2.eval(nt, j):
                        time -= nt.time_trace[j]
                        if self.i.include(time):
                        # if time <= self.tb:
                            return True
                        else:
                            return False
                    else:
                        continue
                else:
                    return False
        return False


class R(PathFormula):
    def __init__(self, i: Interval, phi1: PathFormula, phi2: PathFormula):
        super().__init__()
        if not isinstance(phi1, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        if not isinstance(phi2, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.i = i  # time bound
        self.phi1 = phi1
        self.phi2 = phi2

    def __repr__(self):
        return "R({}, {}, {})".format(self.i, self.phi1, self.phi2)

    def __str__(self):
        return f"{self.phi1} R{self.i} {self.phi2}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        return Not(U(self.i, Not(self.phi1), Not(self.phi2))).eval(nt, k)


class F(PathFormula):
    def __init__(self, i: Interval, phi: PathFormula):
        super().__init__()
        if not isinstance(phi, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.i = i
        self.phi = phi

    def __repr__(self):
        return "F({}, {})".format(self.i, self.phi)

    def __str__(self):
        return f"F{self.i}, {self.phi}"

    def eval(self, nt: NetworkTrace, k: int) -> bool:
        # time = 0
        # for j in range(k, len(nt)):
        #     time += nt.time_trace[j]
        #     if self.phi.eval(nt, j) and time <= self.tb:
        #         return True
        # return False
        return U(self.i, Bool(True), self.phi).eval(nt, k)


class G(PathFormula):
    def __init__(self, i: Interval, phi: PathFormula):
        super().__init__()
        if not isinstance(phi, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.i = i
        self.phi = phi

    def __repr__(self):
        return "G({}, {})".format(self.i, self.phi)

    def __str__(self):
        return f"G{self.i}, {self.phi}"

    def eval(self, ns: NetworkTrace, k: int) -> bool:
        return Not(F(self.i, Not(self.phi))).eval(ns, k)


class P:
    def __init__(self, phi: PathFormula, comparator: str, theta: Optional[float] = None):
        super().__init__()
        if not isinstance(phi, PathFormula):
            raise ValueError("Passed formula has to be path formula")
        self.phi = phi

        if comparator not in ["=?", ">", ">=", "<", "<="]:
            raise ValueError("Wrong comparator")
        self.comparator = comparator

        if theta is not None:
            if theta <= 0 or theta >= 1:
                raise ValueError("Theta should be in (0,1)")
            self.value = theta
        else:
            self.value = None

    def __repr__(self):
        return "P({}, {}, {})".format(self.comparator, self.value, self.phi)

    def __str__(self):
        return f"P{self.comparator}{self.value} {self.phi}"




if __name__ == "__main__":
    from model.networkstate import NetworkState
    from model.networktrace import NetworkTrace
    from model.cptem import CPTEM
    from model.state import State

    s1 = State("work")
    s2 = State("fail")

    c = CPTEM(entity="n1", attr={})
    c.add_states({s1, s2})

    nt = NetworkTrace()

    c.set_current_state(s1)
    ns = NetworkState({'n1': c})

    nt.append(100, ns, None)

    c.set_current_state(s2)
    ns = NetworkState({'n1': c})
    nt.append(110, ns, None)

    # nt = NPTEM.mlag_run()
    ap = AP("s1", "state", "=", "work")
    ap1 = AP("n1", "state", "=", "work")
    ap2 = AP("n1", "state", "=", "fail")
    phi1 = And(ap, ap1)
    phi2 = And(ap, ap2)

    phi = Or(phi1, phi2)

    I = Interval("[", 0, 200, "]")

    phi3 = U(I, ap1, ap2)

    print(nt)
    print(phi3)
    print(phi3.eval(nt, 0))
